#pragma once

/**********************************************************
oxsat - portable sat solver for windows and unix
Copyright (C) 2017  tj bandrowsky

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
*/

#include "decision.h"
#include <vector>
#include <list>
#include "big_int.h"

namespace solver
{
	class literal_node;

	typedef skip_lists::skip_list_type<literal, literal_node *, literal_compare_type> literal_node_list;
	typedef skip_lists::skip_list_type<literal, literal_node *, literal_compare_type>::node_type literal_node_node;

	class literal_node
	{
	public:

		literal_node *parent;
		literal lit;

		// std::list<literal_node *> children;
		literal_node_list children;
		int string_id;
		bool used;

		literal_node() :
			parent(nullptr), 
			string_id(-1),
			used(false),
			children(0,nullptr)
		{
			lit.ref = -1;
			lit.val = 0;
		}

		literal_node( literal_node *_parent, literal _lit, int _string_id ) 
			: parent( _parent ),
			lit( _lit ),
			string_id( _string_id ),
			used(false),
			children(0, nullptr)
		{
			;
		}

		~literal_node()
		{
			;
		}

		decision_string to_string()
		{
			decision_string ds;
			literal_node *p = this;
			while (p->parent != nullptr)
			{
				ds.add(p->lit);
				p = p->parent;
			}
			return ds;
		}
	};


	class decision_string_collection
	{
		int string_id;
		literal_node *root;

		bool find_strings(literal_node *n, decision_string& dstr, std::list<literal_node *>& found_strings)
		{
			bool result = false;

			for (auto childnode = n->children.first(); childnode != nullptr;  childnode = n->children.next(childnode))
			{
				auto child = childnode->value;
				if (dstr.exists_exact(child->lit))
				{
					if (child->string_id) 
					{
						found_strings.push_back(child);
						result = true;
						find_strings(child, dstr, found_strings);
					}
					else 
					{
						bool temp;
						temp = find_strings(child, dstr, found_strings);
						if (temp) 
						{
							result = true;
						}
					}
				}
			}

			return result;
		}

		int add(literal_node *n, decision_string& ds, decision_node *dsn)
		{
			int result = 0;
			if (dsn == nullptr)
			{
				string_id++;
				n->string_id = string_id;
				return string_id;
			}
			const literal& target = dsn->value;
			bool found = false;

			auto found_node = n->children.find(target);

			if (found_node)
			{
				found = true;
				auto dsnn = ds.next(dsn);
				result = add(found_node->value, ds, dsnn);
			}

			if (!found)
			{
				literal_node *new_node = new literal_node(n, target, false);
				n->children.update(target, new_node);
				auto dsnn = ds.next(dsn);
				result = add(new_node, ds, dsnn);
				count++;
			}

			return result;
		}

		void clear(literal_node *n)
		{
			for (auto childnode = n->children.first(); childnode != nullptr; childnode = n->children.next(childnode))
			{
				clear(childnode->value);
			}
			n->children.clear();
			delete n;
		}

		int count;

	public:

		decision_string_collection() : count(0), string_id(0)
		{
			root = new literal_node();
		}

		virtual ~decision_string_collection()
		{
			if (root != nullptr)
			{
				clear(root);
				root = nullptr;
			}
			count = 0;
		}

		void clear()
		{
			string_id = 0;
			clear(root);
			root = new literal_node();
		}

		bool find_strings(decision_string& ds, std::list<literal_node *>& found_strings)
		{
			bool result;
			result = find_strings(root, ds, found_strings);
			return result;
		}

		int add(decision_string& ds)
		{
			int sid = 0;
			sid = add(root, ds, ds.first());
			return sid;
		}
		
		int get_count()
		{
			return count;
		}

		static void self_test(std::list<std::string>& results)
		{
			decision_string_collection collection;

			collection.self_test_impl(results);
		}

		void self_test_impl(std::list<std::string>& results)
		{

			decision_string rule1("ABC");
			decision_string rule2("A!BF");
			decision_string rule3("CD");
			decision_string rule4("!ABD");
			decision_string rule5("!B!E");

			add(rule1);
			add(rule2);
			add(rule3);
			add(rule4);
			add(rule5);

			decision_string test1("!ACE");
			decision_string test2("ABCD");
			decision_string test3("A!BC!E");

			std::list<literal_node *> fn1, fn2, fn3, fn4, fn5, fn6, fn7, fn8, fn9;

			if (!find_strings(rule1, fn1)) 
				results.push_back("decision_string_collection: rule1 invalid");

			if (!find_strings(rule2, fn2))
				results.push_back("decision_string_collection: rule2 invalid");

			if (!find_strings(rule3, fn3))
				results.push_back("decision_string_collection: rule2 invalid");

			if (!find_strings(rule3, fn3))
				results.push_back("decision_string_collection: rule2 invalid");

			if (!find_strings(rule4, fn4))
				results.push_back("decision_string_collection: rule4 invalid");

			if (!find_strings(rule5, fn5))
				results.push_back("decision_string_collection: rule5 invalid");

			// now, should be able to find 2 & 3 but not find 1
			if (find_strings(test1, fn6))
				results.push_back("decision_string_collection: test1 invalid");

			if (!find_strings(test2, fn7))
				results.push_back("decision_string_collection: test2 invalid");

			if (!find_strings(test3, fn8))
				results.push_back("decision_string_collection: test3 invalid");

		}
	};

	class production
	{
	public:
		decision_string match;
		literal product;
		int stringid;
		pdecision source_clause;
	};

	typedef production *pproduction;

	class decision_result
	{
	public:
		bool matched;
	};

	class add_value_result
	{
	public:
		bool success;
	};

	class conflict_mapping 
	{
	public:

		pproduction match_prod;
		packed_big_int match;
		uint64_t add_bit;
		uint64_t fail_count;
		bool outer;

		conflict_mapping() : match_prod(nullptr), fail_count(0), outer(false)
		{

		}
	};

	class variable_mapping
	{
	public:
		int ref;
		int value;
	};

	class variable_root
	{
	public:
		int ref;
		int value_mask;
		uint64_t bitidx;

		variable_root() : ref(-1), value_mask(0), bitidx(0)
		{

		}
	};

	class multiconflict_iterator
	{
	public:
		std::vector<conflict_mapping *> conflicts;
		std::vector<variable_root> variables;
		decision_string variable_index;
		big_int current_value;
		big_int outer_value;
		std::vector<int> outer_value_map;
		bool verbose;

		bool test_conflict(conflict_mapping *cm)
		{
			return current_value.test(&cm->match);
		}

		void fold_values(decision_string& dest)
		{
			decision_string temp;
			get_values(temp);
			dest.fold(temp);
		}

		void get_values(decision_string& dest)
		{
			dest.clear();
			for (int i = 0; i < variables.size(); i++) {
				auto& v = variables[i];
				literal nl;
				nl.ref = v.ref;
				nl.val = current_value.get_bit(v.bitidx);
				dest.add(nl);
			}
		}

		void get_names(decision_string& dest)
		{
			dest.clear();
			for (int i = 0; i < variables.size(); i++) {
				auto& v = variables[i];
				literal nl;
				nl.ref = v.ref;
				nl.val = 1;
				dest.add(nl);
			}
		}

		std::function<void(const char *message)> progress_func;
		decision_string last_result;
		int max_conflicts;

		multiconflict_iterator(int max_conflicts) : max_conflicts( max_conflicts )
		{
		}

		virtual ~multiconflict_iterator()
		{
			clear();
		}

		decision_string get_variables()
		{
			get_values(last_result);
			return last_result;
		}

		void clear()
		{
			for (auto cmi = conflicts.begin(); cmi != conflicts.end(); cmi++)
			{
				auto c = *cmi;
				if (c != nullptr)
					delete c;
			}

			conflicts.clear();
			variables.clear();
			current_value.clear();
		}

		int size()
		{
			return variables.size();
		}

		int add(pproduction prod, bool test)
		{
			for (auto cmi : conflicts) 
			{
				if (cmi->match_prod == prod) 
				{
					return 0;
				}
			}

			if (test) 
			{
				return 1;
			}

			conflict_mapping *cm = new conflict_mapping();
			cm->match_prod = prod;
			cm->fail_count = 0;
			cm->add_bit = 0;
			int64_t bitidx = 0;
			int edge_idx = -1;
			for (auto mpv = prod->match.first(); mpv != nullptr; mpv = prod->match.next(mpv))
			{
				if (!variable_index.exists(mpv->key)) 
				{
					int index = variables.size();
					literal ly;
					ly.ref = mpv->key;
					ly.val = index;
					variable_index.add(ly);
					variable_root vt;
					vt.bitidx = max_variables - index;
					vt.ref = ly.ref;
					vt.value_mask = 0;
					variables.push_back(vt);
				}
				auto v = variable_index.find(mpv->key);

				auto&vx = variables[v->val];
				
				bitidx = vx.bitidx;
				vx.value_mask |= (1 << mpv->value.val);
				cm->match.set_bit(bitidx, mpv->value.val);
				if (!cm->add_bit || cm->add_bit > bitidx)
				{
					cm->add_bit = bitidx;
				}
			}

			conflicts.push_back(cm);

			return 1;
		}

		void init_outer_value()
		{
			outer_value.clear();
			outer_value_map.clear();
			int s = variables.size();
			for (int i = 0; i < s; i++)
			{
				auto& v = variables[i];
				if (v.value_mask == 3) {
					outer_value_map.push_back(v.bitidx);
					for (auto cmi : conflicts)
					{
						if (cmi->add_bit == v.bitidx)
						{
							cmi->outer = true;
						}
					}

				}
			}
		}

		bool step_outer_value()
		{
			outer_value.add(1);
			int s = outer_value_map.size();
			if (outer_value.get_bit(s))
				return false;
			for (int i = 0; i < s; i++)
			{
				int bi = outer_value_map[i];
				uint64_t b = outer_value.get_bit(i);
				current_value.set_bit(bi, b);
			}
		}

		bool has_conflict(pproduction prod)
		{
			for (auto cmi : conflicts)
			{
				if (cmi->match_prod == prod)
				{
					return true;
				}
			}
			return false;
		}

		bool get_first(decision_string& solution)
		{
			for (auto cm : conflicts)
			{
				cm->fail_count = 0;
			}

			current_value.clear();
			init_outer_value();

			do 
			{
				if (verbose) {
					std::cout << "C Outer:" << outer_value.to_string() << std::endl;
				}
			inner_retry:

				if (verbose) {
					std::cout << "C Inner:" << current_value.to_string() << std::endl;
				}

				if (current_value.get_bit(variables.size()))
				{
					current_value.clear();
					continue;
				}

				for (auto cm : conflicts)
				{
					if (test_conflict(cm))
					{
						cm->fail_count++;
						if (cm->outer)
							break;
						else if (current_value.add(cm->add_bit))
							goto inner_retry;
						else {
							get_names(last_result);
							return false;
						}
					}
				}
				get_names(last_result);
				solution.fold(last_result);
				return true;
			} while (step_outer_value());

			get_values(last_result);
			return false;
		}

		bool get_next(decision_string& solution)
		{
			if (!current_value.add(0))
				return false;
				
		retry1:
			for (auto cm : conflicts)
			{
				if (test_conflict(cm))
				{
					cm->fail_count++;
					if (current_value.add(1))
						goto retry1;
					else {
						get_names(last_result);
						return false;
					}
				}
			}

			get_values(last_result);
			solution.fold(last_result);

			return true;
		}

		int64_t get_failed_conflicts(std::list<conflict_mapping *>& fail_list)
		{
			int total = 0;
			for (auto cm : conflicts)
			{
				if (cm->fail_count > 0) 
				{
					fail_list.push_back(cm);
					total += cm->fail_count;
				}
			}
			return total;
		}

		int64_t get_conflict_scale()
		{
			return variables.size();
		}

		big_int get_conflict_idx()
		{
			return current_value;
		}

	};

}
